The present invention relates generally to circuit synthesis verification whereby an implementation based upon a system specification is proven before, for example, an integrated circuit is fabricated. More particularly, it concerns improved method and apparatus for verifying circuits having as part of their specification one or more explicit don""t care conditions or functions.
As the complexity of integrated circuits approaches and exceeds one million transistors, the use of event-driven simulation becomes less and less feasible as a method for validating the timing and functionality of a design. Consequently, designers are developing new methodologies around new tools to replace event-driven simulation whenever possible. They are using cycle-based simulators and emulation at the front end of the design process to ensure that the original register-transfer level (RTL) specification meets their expectations.
Static timing verifiers ensure that the design""s gate-level implementation meets all of its timing requirements at the back end. Formal verification is useful at both ends of the design process. At the front end, it ensures that a refinement of an RTL description is equivalent to the original specification. At the back end, it verifies that the final gate-level description is a valid implementation of the original or modified specification. While these new tools cannot entirely replace event-driven simulation, they can significantly reduce the amount of simulation required for each design. Since designers may use formal verification at many points in the design flow, what is meant by verification may change as the context changes.
Known background publications include the following references, familiarity with which is assumed, which references are incorporated herein by this reference.
[1] D. Brand, xe2x80x9cVerification of Large Synthesized Designs,xe2x80x9d Proc. 1993 IEEE Intl. Conf. on CAD, November 1993, pp. 534-7;
[2] D. Brand, R. A. Bergamaschi, and L. Stok, xe2x80x9cBe Careful with Don""t Cares,xe2x80x9d Proc. 1995 IEEE Intl. Conf. on CAD, November 1995, pp. 83-6;
[3] F. M. Brown, Boolean Reasoning, Kluwer Academic Publishers, Boston, 1990;
[4] R. E. Bryant, xe2x80x9cGraph-based Algorithms for Boolean Function Manipulation,xe2x80x9d IEEE Trans. Computers., vol. 35, no. 8, August 1986, pp. 677-91;
[5] R. E. Bryant, xe2x80x9cOn the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication,xe2x80x9d IEEE Trans. Computers., vol. 40, no. 2, February 1991, pp. 205-13;
[6] E. Cerny, xe2x80x9cAn Approach to a Unified Methodology of Combinational Switching Circuits,xe2x80x9d IEEE Trans. Computers., vol. 26, no. 8, August 1977, pp. 745-56;
[7] J. Jain, R. Mukherjee, and M. Fujita, xe2x80x9cAdvanced Verification Techniques Based on Learning,xe2x80x9d Proc. 32nd ACM/IEEE DAC, June 1995, pp. 420-6;
[8] W. Kunz, xe2x80x9cHANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning,xe2x80x9d Proc. 1993 IEEE Intl. Conf. on CAD, November 1993, pp. 538-43;
[9] Y. Matsunaga, xe2x80x9cAn Efficient Equivalence Checker for Combinational Circuits,xe2x80x9d Proc. 33rd ACM/IEEE DAC, June 1996, pp. 629-34; and
[10] D. Stoffel and W. Kunz, xe2x80x9cLogic Equivalence Checking by Optimization Techniques,xe2x80x9d Proc. Intl. Workshop on CAD, Test and Evaluation for Dependability, July 1996, pp. 85-90.
These background references may be referred to herein by first listed author or by their bracketed number, e.g. the Stoffel et al. article is referred to herein simply as [10].
Bryant made the first major breakthrough in formal verification with the development of ordered binary decision diagrams (OBDDs) [4]. OBDDs are canonical directed graph structures for representing logic functions. They allow us to compare logic functions by comparing their OBDDs. In practice, using OBDDs as a canonical form works well for a large number of functions. There are, however, large classes of important circuits for which the size of the digraph grows exponentially. The most famous of these circuits are multipliers [5].
Most of the recent research in verification has concentrated on verifying circuits which have a reasonable amount of structural similarity. This is usually true of synthesized circuits. These methods try to find points in one circuit which can replace points in the other circuit. The techniques used by these systems include automatic test pattern generation (ATPG) [1], recursive learning [8, 10], and other OBDD-based techniques [7, 9]. All of these techniques either implicitly or explicitly use a structure called a miter during verification. Two versions of miters are shown in FIGS. 1A and 1B. In the left-hand circuit of FIG. 1A, a copy of the specification and a copy of the implementation share common inputs. Their outputs are joined using an exclusive-NOR (XNOR) gate. The specification and the implementation are equivalent if and only if the output of the miter is a tautology, i.e., if the circuit can be reduced to a constant 1.
Notice that there is no don""t care information represented in this circuit. If there were a function d, which represented a set of input conditions for which designers did not care about the values of the output, then they could modify the miter by connecting a network representing d to the output of the XNOR with an OR gate. This is shown in FIG. 1B.
Circuit designers can introduce don""t cares into a network in essentially two ways [2]. First, they can assign an X to a signal in their high-level design language (HDL) source code. While language designers originally intended the X value to represent an unknown value to a simulator, many synthesis systems interpret it as a don""t care. Second, they can assert that an input pattern can never occur. For example, if a module implements the next state logic of a one-hot encoded FSM, they could assert that exactly one state bit should be one at all times. One can represent both of these types of don""t cares schematically using a don""t care cell. This cell has two inputs representing an ordered pair (f, d). The output of the cell evaluates to f when d=0. The output evaluates to X when d=1. FIGS. 2A and 2B show two uses of the don""t care cell. The circuit on the left (FIG. 2A) can be used to generate a logical X value. Since the d function is always 1, the output is always X. The right-hand circuit (FIG. 2B) specifies a function z=axc2x7b, which has a don""t care set of dz=a⊕b. This is equivalent to asserting that a and b must be equal.
Using a don""t care cell to represent incompletely specified functions, designers can represent don""t care information anywhere in a circuit. This would present a problem if they wanted to construct a miter like the one in FIGS. 1A and 1B, because there is no obvious way to construct the don""t care network for the primary outputs.
The specification is organized as follows. In the background section above, some of the issues involved in verification when don""t cares are present in designs are identified. Specifically, the need for propagating don""t care information from internal lines to outputs is demonstrated. In the detailed description to follow, previous formulations for propagating don""t cares through a network will be described. Next, the invented method for representing the propagation of don""t care conditions with a linear space network will be described by reference to FIGS. 3A through 9B. Finally, the issue of designs having explicit don""t care information is addressed. We also show how to use the invented network formulations in several verification contexts. As will be seen, a tremendous advantage of the invented formulation is that it allows existing verification algorithms to work without modification.
The present invention disclosure is not concerned with different methods for performing formal verification. It is concerned with the implications of performing verification in different contexts. Particularly, it is desired to investigate what happens when one compares designs which contain explicit don""t care information on internal lines. In the past, synthesis system designers have ignored the issue of don""t care conditions during verification based on the following assumptions. First, there was an assumption that only one circuitxe2x80x94typically the specificationxe2x80x94had any explicit don""t care information associated with it. Second, the designer could succinctly represent this information with a separate network which represented all input conditions for which the outputs of the circuit could take on any value. Third, there was the assumption that the designer could verify hierarchical blocks in isolation, i.e., the hierarchies of the two designs matched and no optimization occurred across blocks. Therefore, there was no need to propagate don""t care information from one level of a hierarchy to another.
In practice, however, designers cannot make any of these assumptions. When a designer compares two RTL descriptions at the beginning of the design process, both are likely to contain (possibly different) don""t care conditions. Also, a common way to specify don""t care information in HDL is to assign a signal the value X. In effect, this allows the designer to specify don""t care information at internal points of the circuit. Finally, when comparing pre- and post-layout netlists or an RTL to a gate-level netlist, levels of hierarchy are often different. When parts of a design are flattened to make the hierarchies match, don""t care information will again appear at internal lines of the circuit. As will be seen, handling don""t cares under these more realistic conditions is not a trivial matter.
Briefly, the invention may be described as follows. The invented method is for verifying a simulated system""s compliance with a defined system specification, wherein the system specification has explicitly defined don""t care conditions. Preferably, the method includes 1) for each incompletely specified function represented by an ordered pair (f, d) wherein f is an on-set and wherein d is a don""t care set, transforming the ordered pair representation into an interval represented by an ordered pair [m, M] wherein [m, M]={f, m⊂f⊂M}; 2) propagating a set of input conditions through such interval to produce a set of output conditions representative of such on-set and of such don""t care set; and 3) verifying that the set of output conditions meets the defined system specification.
Another way of describing the invented method is as a method for simulating a system containing explicit don""t care functions. Such invented method preferably includes 1) constructing a gate-level implementation of the system including logic gates and don""t care functions represented by cells including at least one cell representing an incompletely specified function; 2) transforming each cell that represents an incompletely specified function characterized by an interval having upper and lower bounds into a plurality of cells that implements the upper and lower bounds of the interval of the incompletely specified function; and 3) tautology-checking the plurality of cells for equality or consistency.
The invented apparatus, quite simply, includes operatively coupled processors, e.g. software processes or code, that cooperate to implement the invented method described briefly above.